Nuprl Lemma : discrete_struct_wf
11,40
postcript
pdf
A
:Type{i}. discrete_struct{i:l}(
A
)
Type{i'}
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
DS(
A
)
Lemmas
deq
wf
origin
A:Type{i}. discrete_struct{i:l}(A) 
Type{i'} A:Type{i}. discrete_struct{i:l}(A) Type{i'} x:A. B(x) T